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

Theorem nfopab1 5126
Description: The first 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
nfopab1 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}

Proof of Theorem nfopab1
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 df-opab 5120 . 2 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
2 nfe1 2145 . . 3 𝑥𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
32nfab 2981 . 2 𝑥{𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
41, 3nfcxfr 2972 1 𝑥{⟨𝑥, 𝑦⟩ ∣ 𝜑}
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1528  wex 1771  {cab 2796  wnfc 2958  cop 4563  {copab 5119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-opab 5120
This theorem is referenced by:  nfmpt1  5155  rexopabb  5406  opelopabsb  5408  ssopab2bw  5425  ssopab2b  5427  0nelopab  5443  dmopab  5777  rnopab  5819  funopab  6383  fvopab5  6792  zfrep6  7645  opabdm  30290  opabrn  30291  fpwrelmap  30395  vvdifopab  35402  aomclem8  39539  sprsymrelf  43534
  Copyright terms: Public domain W3C validator