Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfopab2 Structured version   Visualization version   GIF version

Theorem nfopab2 4753
 Description: The second abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free. (Contributed by NM, 16-May-1995.) (Revised by Mario Carneiro, 14-Oct-2016.)
Assertion
Ref Expression
nfopab2 𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}

Proof of Theorem nfopab2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-opab 4746 . 2 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
2 nfe1 2067 . . . 4 𝑦𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
32nfex 2192 . . 3 𝑦𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
43nfab 2798 . 2 𝑦{𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
51, 4nfcxfr 2791 1 𝑦{⟨𝑥, 𝑦⟩ ∣ 𝜑}
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   = wceq 1523  ∃wex 1744  {cab 2637  Ⅎwnfc 2780  ⟨cop 4216  {copab 4745 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-opab 4746 This theorem is referenced by:  opelopabsb  5014  ssopab2b  5031  dmopab  5367  rnopab  5402  funopab  5961  fvopab5  6349  0neqopab  6740  zfrep6  7176  opabdm  29549  opabrn  29550  fpwrelmap  29636  vvdifopab  34165  aomclem8  37948  areaquad  38119  sprsymrelf  42070
 Copyright terms: Public domain W3C validator