Theorem ralrn 7099

Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)

Hypothesis

Ref	Expression
rexrn.1	⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralrn	⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem ralrn

Step	Hyp	Ref	Expression
1		fvexd 6911	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6956	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2770	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3113	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 290	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 487	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5376	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2146  ∀wral 3080  ∃wrex 3090  Vcvv 3454  ran crn 5656   Fn wfn 6542  ‘cfv 6547

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6501  df-fun 6549  df-fn 6550  df-fv 6555

This theorem is used by:  ralrnmptw  7105  ralrnmpt  7107  cbvfo  7307  isoselem  7359  fnwe2lem3  8160  indexfi  9363  ordtypelem9  9533  ordtypelem10  9534  wemapwe  9711  numacn  10141  acndom  10143  rpnnen1lem3  13120  fsequb2  14132  limsuple  15660  limsupval2  15662  climsup  15852  ruclem11  16423  ruclem12  16424  prmreclem6  17114  imasaddfnlem  17715  imasvscafn  17724  cycsubgcl  19436  ghmrn  19458  ghmnsgima  19469  pgpssslw  19843  gexex  20082  dprdfcntz  20246  znf1o  21872  frlmlbs  22118  lindfrn  22142  ptcnplem  23955  kqt0lem  24070  isr0  24071  regr1lem2  24074  uzrest  24231  tmdgsum2  24430  imasf1oxmet  24709  imasf1omet  24710  bndth  25294  evth  25295  ovolficcss  25805  ovollb2lem  25824  ovolunlem1  25833  ovoliunlem1  25838  ovoliunlem2  25839  ovoliun2  25842  ovolscalem1  25849  ovolicc1  25852  voliunlem2  25887  voliunlem3  25888  ioombl1lem4  25897  uniioovol  25915  uniioombllem2  25919  uniioombllem3  25921  uniioombllem6  25924  volsup2  25941  vitalilem3  25946  mbfsup  26000  mbfinf  26001  mbflimsup  26002  itg1ge0  26022  itg1mulc  26040  itg1climres  26050  mbfi1fseqlem4  26054  itg2seq  26078  itg2monolem1  26086  itg2mono  26089  itg2i1fseq2  26092  itg2gt0  26096  itg2cnlem1  26097  itg2cn  26099  limciun  26229  plycpn  26625  hmopidmchi  32768  hmopidmpji  32769  rge0scvg  34637  mclsax  36458  mblfinlem2  38722  ismtyhmeolem  38884  nacsfix  43869  gneispace  45280  climinf  46763  liminfval2  46923